Termination w.r.t. Q of the following Term Rewriting System could not be shown:
Q restricted rewrite system:
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
↳ QTRS
↳ DependencyPairsProof
Q restricted rewrite system:
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
Q DP problem:
The TRS P consists of the following rules:
IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, in_2, st_2, tail1(in_3), st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_2)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> TAIL1(in_3)
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, st_2)
IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> TAIL1(in_3)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> HEAD1(in_3)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(two, head1(in_2))
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, tail1(in_2), st_2, in_3, st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, app2(map_f2(three, head1(in_3)), st_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(two, head1(in_2)), st_2)
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> TAIL1(in_2)
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(three, head1(in_3)), st_3)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> MAP_F2(two, head1(in_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LENGTH1(st_2)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> EMPTY1(fstsplit2(m, st_2))
APP2(cons2(h, t), x) -> APP2(t, x)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(map_f2(two, head1(in_2)))
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, st_1)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_3)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> EMPTY1(fstsplit2(m, st_3))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3)))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(two, head1(in_2))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(three, head1(in_3)), st_3)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_3)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(three, head1(in_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LEQ2(m, length1(st_3))
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_3)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LEQ2(m, length1(st_2))
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> FSTSPLIT2(m, st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> FSTSPLIT2(m, st_3)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LENGTH1(st_3)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> MAP_F2(three, head1(in_3))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(map_f2(three, head1(in_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(fstsplit2(m, st_1))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> TAIL1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> HEAD1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_1)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(three, head1(in_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(three, head1(in_3)), st_3))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> FSTSPLIT2(m, st_1)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(two, head1(in_2)), st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
Q DP problem:
The TRS P consists of the following rules:
IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, in_2, st_2, tail1(in_3), st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_2)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> TAIL1(in_3)
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, st_2)
IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> TAIL1(in_3)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> HEAD1(in_3)
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(two, head1(in_2))
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, tail1(in_2), st_2, in_3, st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, app2(map_f2(three, head1(in_3)), st_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(two, head1(in_2)), st_2)
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> TAIL1(in_2)
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(three, head1(in_3)), st_3)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> MAP_F2(two, head1(in_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LENGTH1(st_2)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> EMPTY1(fstsplit2(m, st_2))
APP2(cons2(h, t), x) -> APP2(t, x)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(map_f2(two, head1(in_2)))
LENGTH1(cons2(h, t)) -> LENGTH1(t)
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, st_1)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_3)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> EMPTY1(fstsplit2(m, st_3))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3)))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(two, head1(in_2))
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(three, head1(in_3)), st_3)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_3)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(three, head1(in_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(two, head1(in_2)), st_2))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LEQ2(m, length1(st_3))
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_3)
MAP_F2(pid, cons2(h, t)) -> APP2(f2(pid, h), map_f2(pid, t))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> HEAD1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LEQ2(m, length1(st_2))
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> FSTSPLIT2(m, st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> FSTSPLIT2(m, st_3)
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> LENGTH1(st_3)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> MAP_F2(three, head1(in_3))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(map_f2(three, head1(in_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> EMPTY1(fstsplit2(m, st_1))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> TAIL1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> HEAD1(in_2)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> SNDSPLIT2(m, st_1)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> MAP_F2(three, head1(in_3))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> EMPTY1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> FSTSPLIT2(m, app2(map_f2(three, head1(in_3)), st_3))
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> FSTSPLIT2(m, st_1)
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> APP2(map_f2(two, head1(in_2)), st_2)
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The approximation of the Dependency Graph contains 7 SCCs with 45 less nodes.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
APP2(cons2(h, t), x) -> APP2(t, x)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
APP2(cons2(h, t), x) -> APP2(t, x)
Used argument filtering: APP2(x1, x2) = x1
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
MAP_F2(pid, cons2(h, t)) -> MAP_F2(pid, t)
Used argument filtering: MAP_F2(x1, x2) = x2
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LENGTH1(cons2(h, t)) -> LENGTH1(t)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
LENGTH1(cons2(h, t)) -> LENGTH1(t)
Used argument filtering: LENGTH1(x1) = x1
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
LEQ2(s1(n), s1(m)) -> LEQ2(n, m)
Used argument filtering: LEQ2(x1, x2) = x2
s1(x1) = s1(x1)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
SNDSPLIT2(s1(n), cons2(h, t)) -> SNDSPLIT2(n, t)
Used argument filtering: SNDSPLIT2(x1, x2) = x2
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using an argument filtering and a montonic ordering, at least one Dependency Pair of this SCC can be strictly oriented.
FSTSPLIT2(s1(n), cons2(h, t)) -> FSTSPLIT2(n, t)
Used argument filtering: FSTSPLIT2(x1, x2) = x2
cons2(x1, x2) = cons1(x2)
Used ordering: Quasi Precedence:
trivial
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDPAfsSolverProof
↳ QDP
↳ PisEmptyProof
↳ QDP
Q DP problem:
P is empty.
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
The TRS P is empty. Hence, there is no (P,Q,R) chain.
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
↳ QDP
Q DP problem:
The TRS P consists of the following rules:
IF_97(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, in_2, st_2, tail1(in_3), st_3, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
IF_57(st_1, in_2, st_2, in_3, st_3, m, true) -> RING6(st_1, tail1(in_2), st_2, in_3, st_3, m)
IF_67(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
IF_27(st_1, in_2, st_2, in_3, st_3, m, false) -> IF_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
IF_77(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
IF_37(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
IF_17(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
IF_87(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
IF_27(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
IF_47(st_1, in_2, st_2, in_3, st_3, m, false) -> RING6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
RING6(st_1, in_2, st_2, in_3, st_3, m) -> IF_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
IF_67(st_1, in_2, st_2, in_3, st_3, m, true) -> IF_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
The TRS R consists of the following rules:
fstsplit2(0, x) -> nil
fstsplit2(s1(n), nil) -> nil
fstsplit2(s1(n), cons2(h, t)) -> cons2(h, fstsplit2(n, t))
sndsplit2(0, x) -> x
sndsplit2(s1(n), nil) -> nil
sndsplit2(s1(n), cons2(h, t)) -> sndsplit2(n, t)
empty1(nil) -> true
empty1(cons2(h, t)) -> false
leq2(0, m) -> true
leq2(s1(n), 0) -> false
leq2(s1(n), s1(m)) -> leq2(n, m)
length1(nil) -> 0
length1(cons2(h, t)) -> s1(length1(t))
app2(nil, x) -> x
app2(cons2(h, t), x) -> cons2(h, app2(t, x))
map_f2(pid, nil) -> nil
map_f2(pid, cons2(h, t)) -> app2(f2(pid, h), map_f2(pid, t))
head1(cons2(h, t)) -> h
tail1(cons2(h, t)) -> t
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_17(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_1)))
if_17(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(sndsplit2(m, st_1), cons2(fstsplit2(m, st_1), in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_27(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_2)))
if_27(st_1, in_2, st_2, in_3, st_3, m, true) -> if_37(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_2)))
if_37(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, sndsplit2(m, st_2), cons2(fstsplit2(m, st_2), in_3), st_3, m)
if_27(st_1, in_2, st_2, in_3, st_3, m, false) -> if_47(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2))))
if_47(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, tail1(in_2), sndsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), cons2(fstsplit2(m, app2(map_f2(two, head1(in_2)), st_2)), in_3), st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_57(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(two, head1(in_2))))
if_57(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, tail1(in_2), st_2, in_3, st_3, m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_67(st_1, in_2, st_2, in_3, st_3, m, leq2(m, length1(st_3)))
if_67(st_1, in_2, st_2, in_3, st_3, m, true) -> if_77(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, st_3)))
if_77(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, in_3, sndsplit2(m, st_3), m)
if_67(st_1, in_2, st_2, in_3, st_3, m, false) -> if_87(st_1, in_2, st_2, in_3, st_3, m, empty1(fstsplit2(m, app2(map_f2(three, head1(in_3)), st_3))))
if_87(st_1, in_2, st_2, in_3, st_3, m, false) -> ring6(st_1, in_2, st_2, tail1(in_3), sndsplit2(m, app2(map_f2(three, head1(in_3)), st_3)), m)
ring6(st_1, in_2, st_2, in_3, st_3, m) -> if_97(st_1, in_2, st_2, in_3, st_3, m, empty1(map_f2(three, head1(in_3))))
if_97(st_1, in_2, st_2, in_3, st_3, m, true) -> ring6(st_1, in_2, st_2, tail1(in_3), st_3, m)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.